Looks good to me. Thanks for the contribution!
But NB #2423 and its antecedents #2365 #2359 etc. Would this proof simplify if we could successfully refactor the definition of partition? UPDATED: I tried it, and apparently not. Oh well.

My only worry is that given that foldr can encode any function, should we have such a
lemma no matter how complex the cons step is? Relatedly, do we want to simplify this
one by defining e.g.

inj : Bool → A → A ⊎ A
_⊎∷_ : A ⊎ B → List A × List B → List A × List B

partition P? = foldr (\ x -> inj (does P? x) x ⊎∷_) ([], [])

@gallais

I think there is indeed a question as why the definitions are given in Data.List.Base are given in 'plain' form, and not as instances of fold, but given that they are, it makes/made sense to me to accompany each of them with a lemma of this kind. But if we are going to widen the discussion to consider all of those definitions in the library, then... maybe a separate library-design issue worth opening?

As for the (straw-man?) refactoring you propose, I think it falls to Occam's Razor?

I wouldn't call this partition-is-foldr but partition-as-foldr , or partition-via-foldr. And yes, foldr being the List eliminator, we need to be careful to not have an explosion of these. Having said that, I'm fine with partition as it is an important function.

I wouldn't call this partition-is-foldr but partition-as-foldr , or partition-via-foldr. And yes, foldr being the List eliminator, we need to be careful to not have an explosion of these. Having said that, I'm fine with partition as it is an important function.

But we already have

• id-is-foldr
• ++-is-foldr
• map-is-foldr
• ...

So it does explode into a deprecation-fest if we follow your lead? v3.0?

Sigh - yes, v3.0. Inconsistency is worse than misleading names.